$\forall$$A$, $B$:Type, $f$:($A$$\rightarrow$($B$ + Top)), $P$:($A$$\rightarrow\mathbb{P}$), $p$:($\forall$$x$:$A$. Dec($P$($x$))), $x$:$A$.
\\[0ex]($\uparrow$can{-}apply(p{-}co{-}restrict($f$;$p$);$x$)) $\Rightarrow$ (do{-}apply(p{-}co{-}restrict($f$;$p$);$x$) = do{-}apply($f$;$x$) $\in$ $B$)